(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(declare-fun f () Bool)
(declare-fun e () Bool)
(declare-fun g () String)
(declare-fun h () String)
(declare-fun i () Bool)
(declare-fun j () Bool)
(declare-fun k () Bool)
(declare-fun l () Bool)
(declare-fun m () Bool)
(declare-fun n () Bool)
(declare-fun o () String)
(declare-fun p () Bool)
(assert (distinct (= b k) (distinct "-" (str.substr g 0 (str.len o)))))
(assert (distinct i (= a j)))
(assert (distinct d (= e n)))
(assert (distinct (= b p) (distinct "-" (str.substr g 4 (str.len o)))))
(assert (= l (= b p) m (distinct "" (str.substr g 0 (str.len o))) (= f i)))
(assert (distinct c l))
(assert (distinct b (distinct k p)))
(assert (= c (distinct m p)))
(check-sat)
